Nuprl Lemma : ma-single-pre1_wf
0,22
postcript
pdf
a
:Id,
T
,
A
:Type,
x
:Id,
P
:(
A
T
Prop). ma-single-pre1(
x
;
A
;
a
;
T
;
x
,
v
.
P
(
x
,
v
))
MsgA
latex
Definitions
IdDeq
,
x
dom(
f
)
,
f
(
x
)
,
MsgA
,
Prop
,
ma-single-pre1(
x
;
A
;
a
;
T
;
y
,
v
.
P
(
y
;
v
))
,
(with ds:
ds
action
a
:
T
precondition
a
(v) is
P
s v)
,
x
,
y
.
t
(
x
;
y
)
,
x
.
t
(
x
)
,
State(
ds
)
,
x
:
v
,
Id
,
x
:
A
.
B
(
x
)
,
P
Q
,
f
(
x
)?
z
,
x
(
s1
,
s2
)
,
t
T
Lemmas
ma-state
wf
,
Id
wf
,
fpf-single
wf
,
ma-single-pre
wf
,
id-deq
wf
,
eqof
eq
btrue
origin
a:Id, T, A:Type, x:Id, P:(A
TProp). ma-single-pre1(x;A;a;T;x,v.P(x,v)) 
MsgA a:Id, T, A:Type, x:Id, P:(ATProp). ma-single-pre1(x;A;a;T;x,v.P(x,v)) MsgA dom(f)
x,y. t(x;y)x. t(x)x:A. B(x)
Q T